PRISM

./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 zeroconf.prism zeroconf.props --property correct_min -const N=1000,K=8,reset=false

PRISM
=====

Version: 4.5.dev
Date: Sun Mar 15 03:20:26 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 zeroconf.prism zeroconf.props --property correct_min -const 'N=1000,K=8,reset=false'

Parsing model file "zeroconf.prism"...

Type:        MDP
Modules:     environment host0 
Variables:   b_ip7 b_ip6 b_ip5 b_ip4 b_ip3 b_ip2 b_ip1 b_ip0 n n0 n1 b z ip_mess x y coll probes mess defend ip l 

Parsing properties file "zeroconf.props"...

2 properties:
(1) "correct_max": Pmax=? [ F (l=4&ip=1) ]
(2) "correct_min": Pmin=? [ F (l=4&ip=1) ]

---------------------------------------------------------------------

Model checking: "correct_min": Pmin=? [ F (l=4&ip=1) ]
Model constants: reset=false,N=1000,K=8

Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).

Building model...
Model constants: reset=false,N=1000,K=8

Computing reachable states...

Reachability (BFS): 592 iterations in 69.15 seconds (average 0.116814, setup 0.00)

Time for model construction: 70.105 seconds.

Type:        MDP
States:      1870338 (1 initial)
Transitions: 4245554
Choices:     3443961

Transition matrix: 154038 nodes (6 terminal), 4245554 minterms, vars: 58r/58c/7nd

Prob0E: 133 iterations in 5.25 seconds (average 0.039459, setup 0.00)

Prob1A: 91 iterations in 3.11 seconds (average 0.034176, setup 0.00)

yes = 17943, no = 611330, maybe = 1241065

Computing remaining probabilities...
Engine: Sparse
Note: Interval iteration is configured to enforce monotonicity from below.

Building sparse matrix... [n=1870338, nc=2315321, nnz=2865855, k=4] [36.8 MB]
Creating vector for yes... [14.3 MB]
Creating vector for maybe... [14.3 MB]
Allocating iteration vectors... [4 x 14.3 MB]
TOTAL: [122.4 MB]

Starting iterations (interval iteration)...
Iteration 86: max relative diff=1.000000, 5.03 sec so far
Iteration 170: max relative diff=1.000000, 10.05 sec so far
Iteration 254: max relative diff=0.999921, 15.05 sec so far
Iteration 338: max relative diff=0.945684, 20.08 sec so far
Iteration 422: max relative diff=0.148239, 25.12 sec so far
Iteration 506: max relative diff=0.002620, 30.14 sec so far
Iteration 593: max relative diff=0.000029, 35.18 sec so far
Max relative diff between upper and lower bound on convergence: 9.64921E-07
Iterative method (interval iteration): 621 iterations in 40.45 seconds (average 0.059171, setup 3.70)

Value in the initial state: 5.040105212929842E-9

Time for model checking: 48.987 seconds.

Result: 5.040105212929842E-9 (value in the initial state)


Overall running time: 119.693 seconds.

---------------------------------------------------------------------

Note: There was 1 warning during computation.